package systemfnomabss



trait systemfnomabssSubstitution extends systemfnomabss.syntax.Substitution with TermSubstitutionProvider{ self: systemfnomabssSubstitution with systemfnomabss.AbstractSyntax =>



    type substitution[T] = Name => Option[T]
    
    trait PolyFunction1 { 
      def apply[T](t:T):T
    }
    trait PartialPolyFunction1 {
      def isDefinedAt[T](t:T):Boolean
      def apply[T](t:T):T
      def orElse(second:PartialPolyFunction1) = new HigherToLowerPrecedencePartialPolyFunction1(this,second)
    }
    class HigherToLowerPrecedencePartialPolyFunction1(higher:PartialPolyFunction1,lower:PartialPolyFunction1) extends PartialPolyFunction1 {
      def isDefinedAt[T](t:T):Boolean = higher.isDefinedAt(t) || lower.isDefinedAt(t)
      def apply[T](t:T):T = if (higher.isDefinedAt(t)) higher.apply(t) else if (lower.isDefinedAt(t))lower.apply(t) 
                            else throw new Exception("wrong application in HigherPrecedencePartial..  arg = "+t)
    }
    
    object Except {
      def apply[Upto](caseblock:PartialFunction[Upto,Upto]):PartialPolyFunction1
      = new PartialPolyFunction1{
            def isDefinedAt[T](t:T):Boolean = t match {case st:Upto => caseblock.isDefinedAt(st);case _ => false}//erased
            def apply[T](t:T):T = try { t match {case st:Upto =>caseblock(st).asInstanceOf[T]} 
                                    }
                                catch {
                                  case e:java.lang.ClassCastException => 0 to 5 foreach {case _ => println("*")}
                                                                         throw new Exception("In Except to PartialPolyFunction1",e)
                                }                     
        }
    }






type partial = bruijnpart
type topsubst = bruijntopsubst

import sybrevolutions.forvalues.{TypeMan,Typed,ValSpine,ConstrExt,Apped}


object termintoterm_scope {
   
  
  

 //provide for binding case
 def LTermTakesLTermParam(self:LTerm): LTerm CanSubstIn LTerm = new TermintoTermSubstable(self:LTerm)
 //provide for call to specificsubst
 val findTermManhere = TypeManDefs.LTermTypeMan 
 
 class TermintoTermSubstable(self:LTerm) extends (LTerm CanSubstIn LTerm) {
      
      def subst(sub: Name => Option[LTerm]): LTerm 
         = { specificSubstituteWithTerm[LTerm](sub, self)(findTermManhere) }
      
      
      //function that gets called on children:
      // if a hasvar => perform substitution and getorelse
      // if a binds => perform substitution
      // if something which overrides in another way
      // if something else: a general thing => convert to valspine, call general function with this function itself to perform on children

      def specificSubstituteWithTerm[T](sub: substitution[LTerm], t:T)(implicit tman:TypeMan[T]):T = {
            
            //first any exceptions
            val excclauses = Except [Any] { 
              case r@Record(fields) => 
                Record(fields.map( {case (lbl,term) => (lbl, specificSubstituteWithTerm[LTerm](sub,term)(findTermManhere)) }))
              case typ:LType => typ // because ltypes do not take lterms
            }
            //then we get the variable case 
            val variableclause = Except[Any] {
              case dis @RefersByName(n) => (sub(n)).getOrElse(dis)
            } 
            //then the redirect to the general cases
            val general = Except[T] {
              case general => GenericLTermIntoTSubst(tman.toValSpine(general),sub).buildFromSpine
            }
            
            val combined = excclauses orElse variableclause orElse general
            tman match {
              case TypeManDefs.BindsTermTypeMan => 
                             (new AbsTakesSubstitution[LTerm]).AbsIsSubstable(t)(LTermTakesLTermParam).subst(sub)
              case _   => combined[T](t)
            }
      }
      
      def GenericLTermIntoTSubst[T](vs:ValSpine[T], sub: substitution[LTerm]):ValSpine[T] = vs match{
          case c@ConstrExt(_,_) => c
          case Apped(deep,Typed(arg,argtman)) => { 
            implicit val findTMan = argtman
            val argmod = specificSubstituteWithTerm(sub,arg)
            Apped(GenericLTermIntoTSubst(deep,sub), Typed(argmod,argtman)) }
      }
    }
}







object typeintoany_scope{
  
  
 
    val findLTermTypeManhere = TypeManDefs.LTermTypeMan 
    val findLTypeTypeManhere = TypeManDefs.LTypeTypeMan 
  
    def LTermTakesLTypeParam(self:LTerm): LType CanSubstIn LTerm = new (LType CanSubstIn LTerm) {
      def subst(sub: Name => Option[LType]): LTerm= { specificSubstituteWithLType[LTerm](sub, self)(findLTermTypeManhere)}
    }
    def LTypeTakesLTypeParam(self:LType): LType CanSubstIn LType = new (LType CanSubstIn LType) {
      def subst(sub: Name => Option[LType]): LType= { specificSubstituteWithLType[LType](sub, self)(findLTypeTypeManhere)}
    }
    
    def specificSubstituteWithLType[T](sub: substitution[LType], t:T)(implicit tman:TypeMan[T] ):T = {
        val excclauses = Except [Any] { 
          case r@Record(fields) => 
            Record(fields.map ( {case (lbl,term) => (lbl, specificSubstituteWithLType[LTerm](sub,term)(findLTermTypeManhere)) }))
          case TyRecord(fields) =>
            TyRecord(fields.map({case (lbl,ty)   => (lbl, specificSubstituteWithLType[LType](sub,ty)(findLTypeTypeManhere) )  }))
        }
        val varclauses = Except[Any] {
          case dis @RefersByName(n) => (sub(n)).getOrElse(dis)
        }
        val general = Except[T] {
            case general => {
              GenericLTypeIntoTSubst(tman.toValSpine(general),sub).buildFromSpine
            }
        }
        val combined = excclauses orElse varclauses orElse general
        tman match {
              case TypeManDefs.BindsTermTypeMan => 
                     (new AbsTakesSubstitution[LType]).AbsIsSubstable(t)(LTermTakesLTypeParam).subst(sub)
              case TypeManDefs.BindsTypeTypeMan =>
                     (new AbsTakesSubstitution[LType]).AbsIsSubstable(t)(LTypeTakesLTypeParam).subst(sub)
              case _   =>  combined[T](t) 
        }
    }
  
  def GenericLTypeIntoTSubst[T](vs:ValSpine[T], sub: substitution[LType]):ValSpine[T] = vs match{
    case c@ConstrExt(_,_) => c
    case Apped(deep,Typed(arg,argtman)) => {
      implicit val findTMan = argtman
      val argmod = specificSubstituteWithLType(sub,arg)
      Apped(GenericLTypeIntoTSubst(deep,sub), Typed(argmod,argtman)) }
  }
  
}


  

//type Term = LTerm
//type Type = LType
def substituteterm(v:Term)=new bruijnpart(v)
def substitutetype(v:Type)=new bruijnpart(v)
class bruijnpart(v:Node) extends termexamplepartial(v) {
  //def asTop() = new bruijntopsubst(v)
  def as(n:Name) = new bruijntopsubst(n,v) 
}

class bruijntopsubst(n:Name, v:Node) extends termexamplenamesubst(n,v) {
  import termintoterm_scope.{LTermTakesLTermParam}
  import typeintoany_scope.{LTermTakesLTypeParam, LTypeTakesLTypeParam}
  
  def intoterm(term: Term)= (v,term) match {
    case (v:Type,t:Term)  => LTermTakesLTypeParam(t) subst {(name:Name)=> if (name == n) Some(v) else None}
    case (v:Term,t:Term)  => LTermTakesLTermParam(t) subst {(name:Name)=> if (name == n) Some(v) else None}
  }

  def intotype(ty: Type) = (v,ty) match {
    case (v:Type, ty:Type) => LTypeTakesLTypeParam(ty) subst {(name:Name)=> if (name == n) Some(v) else None}
    case (v:Term, ty:Type) => throw new Error("cannot form dependent type")
  }
}


}




object Test extends  systemfnomabssSubstitution with AbstractSyntax with Application {
  val x = Name("x")
  val y = Name("y")
  val z = Name("z")
  import termintoterm_scope.{LTermTakesLTermParam}
  import typeintoany_scope.{LTermTakesLTypeParam, LTypeTakesLTypeParam}
  
  val subXtoZ = LTermTakesLTermParam(Lam(TyBool(),y\\Var(x))) subst (t => if(t == x) Some(Var(z)) else None)
  val subNop = LTermTakesLTermParam(Lam(TyBool(),x\\Var(x))) subst (t => if(t == x) Some(Var(z)) else None);
  val subType = LTermTakesLTypeParam((Lam(TyVar(y),z\\Var(x)))) subst (t => if(t==y) Some(TyBool()) else None);
  val subOnlyType =  LTypeTakesLTypeParam(TyVar(y)) . subst(t => if (t == y) Some(TyBool()) else None);
  val subOnlyType2 = LTypeTakesLTypeParam( TyUniv(x\\TyArr(TyBool(),TyVar(x))) ) . subst(t => if (t== x) Some(TyInt()) else None);
  val subOnlyType3 = LTypeTakesLTypeParam( TyUniv(x\\TyArr(TyBool(),TyVar(y))) ) . subst(t => if (t== y) Some(TyInt()) else None);
  val subOnlyType4 = LTypeTakesLTypeParam( TyUniv(x\\TyArr(TyBool(),TyVar(y))) ) . subst(t => if (t== y) Some(TyVar(x)) else None);
  val subTLamHit =  LTermTakesLTypeParam(TLam(x\\Lam(TyVar(x),y\\Var(y)))) subst( t => if (t == x) Some(TyInt()) else None);
  println( Lam(TyBool(),x\\Var(y)) == Lam (TyBool(),z\\Var(y)),
      Lam(TyBool(),x\\Var(y)) == Lam (TyBool(),y\\Var(x)),
      Lam(TyBool(),x\\Var(x)) == Lam (TyBool(),y\\Var(y)), subXtoZ, subNop,subType)
  println(subOnlyType  + (if (subOnlyType == TyBool()) "  OK" else "  should be TyBool()"))
  println(subOnlyType2 + (if (subOnlyType2 == TyUniv(x\\TyArr(TyBool(),TyVar(x)))) "  OK" else "  should be "+ TyUniv(x\\TyArr(TyBool(),TyVar(x))))) 
  println(subOnlyType3 + (if (subOnlyType3 == TyUniv(x\\TyArr(TyBool(),TyInt()))) "  OK" else "  should be "+ TyUniv(x\\TyArr(TyBool(),TyInt()))) )
  println(subOnlyType4 + (if (subOnlyType4 == TyUniv(x\\TyArr(TyBool(),TyVar(Name("x"))))) "  OK" else "  should be "+ TyUniv(x\\TyArr(TyBool(),TyVar(Name("x"))))) )//wrong, how to introduce new x? just compare toString?
  println(subTLamHit + (if (subTLamHit == TLam(x\\Lam(TyVar(x),y\\Var(y)))) "  OK" else "  should be "+  TLam(x\\Lam(TyVar(x),y\\Var(y)))))
  /*
  println((for(
      x <- gensym("x");
      y <- gensym("y");
      z <- gensym("z");
      subXtoZ <- LTermSubst(Lam(TyBool,y\\Var(x))) subst (t => if(t == x) Some(Var(z)) else None);
      subNop <- LTermSubst(Lam(TyBool,x\\Var(x))) subst (t => if(t == x) Some(Var(z)) else None);
      subType <- LTermTakesLTypeParam((Lam(TyVar(y),z\\Var(x)))) subst (t => if(t==y) Some(TyBool) else None);
      subOnlyType <- TyVar(y) . subst(t => if (t == y) Some(TyBool) else None);
      subTLamHit <- LTermTakesLTypeParam(TLam(x\\Lam(TyVar(x),y\\Var(y)))) subst( t => if (t == x) Some(TyInt) else None))
    yield (Lam(TyBool,x\\Var(y)) == Lam (TyBool,z\\Var(y)),
           Lam(TyBool,x\\Var(y)) == Lam (TyBool,y\\Var(x)),
           Lam(TyBool,x\\Var(x)) == Lam (TyBool,y\\Var(y)), subXtoZ, subNop,subType,
           subOnlyType,
           subTLamHit
           )).run) // prints "(true,false,true,Lam(y$0\\Var(z$2)),Lam(x$0\\Var(x$0)))"
   */
}
